-
Notifications
You must be signed in to change notification settings - Fork 73
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Witgen: Handle machine calls with side effects #1388
Conversation
// TODO: This would be the right thing to do, but currently leads to failing tests | ||
// due to #1385 ("Witgen: Block machines "forget" that they already completed a block"): | ||
// https://github.com/powdr-labs/powdr/issues/1385 | ||
// let updates = updates.report_side_effect(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
test_data/asm/book/operations_and_links.asm
fails, because there is a machine that calls the same sub-machine with multiple arguments. Because of #1385, this keeps adding new blocks. Not reporting the side effect makes this works, because then the identity is not processed again.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
is it gonna be fixed here or later?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Later, this requires fixing #1385, which is not the scope of this PR. The fix in this PR is disabled for block machines because of #1385, but IMO it makes sense to merge like this because it adds all the infrastructure to handle side effects, and it already works for other machines (crucially: memory).
mstore 3, 3; | ||
mstore 4, 4; | ||
|
||
return; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add some assertions so we know the memory proxy is working>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, not sure how to do this actually, because we don't have a shared memory yet (which requires #1356) ^^ So we can't access the memory from the main machine here.
If witgen didn't insert the right memory accesses into the memory machine, the permutation would fail, which is tested by the current test.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ah right
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
left some small comments, otherwise looks good
Cherry-picked ef6a72f from #1380.
With this PR, we track whether a call to a machine led to some side effect (e.g. added a block). In that case, the processed identity should count has having led to some progress, even if no values were returned to the calling machine. An example would be writing values to memory, which does not return any values and hence does not change the state of the caller.